Страница 4 из 6 Вместо доказательства этих утверждений опишем простую процедуру преобразования. Проиллюстрируем эту процедуру, преобразовав высказывание R2, или , в форму CNF. Ниже описаны соответствующие этапы. 1. Устранить связку заменив высказывание высказыванием ![](http://rriai.org.ru/illustr/ai2-241.jpg) 2. Устранить связку заменив высказывание высказыванием ![](http://rriai.org.ru/illustr/ai2-244.jpg) 3. Конъюнктивная нормальная форма требует, чтобы связка появлялась только перед литералами, поэтому, как принято называть эту операцию, "введем связку внутрь выражения", повторяя операцию применения следующих эквивалентностей из листинга 7.4: ![](http://rriai.org.ru/illustr/ai2-247.jpg) В данном примере требуется применение только одного, последнего правила: ![](http://rriai.org.ru/illustr/ai2-248.jpg) 4. В результате получено высказывание, содержащее вложенные связки л и ν, которые применяются к литералам. Используем закон дистрибутивности, приведенный в листинге 7.4, распределяя связки ν по связкам л везде, где это возможно. ![](http://rriai.org.ru/illustr/ai2-249.jpg) Теперь первоначальное высказывание представлено в форме CNF, как конъюнкция трех выражений. Это высказывание стало более сложным для чтения, но зато его можно использовать в качестве входных данных для процедуры резолюции. Алгоритм резолюции Процедуры логического вывода, основанные на правиле резолюции, действуют с использованием принципа доказательства путем установления противоречия, который описывался в конце раздела 7.4. Таким образом, чтобы показать, что мы покажем, что высказывание является невыполнимым. Это можно сделать, доказав, что имеет место противоречие.
|